The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
logarithm(x) → logIter(x, 0) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1]
if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
f → g [1]
f → h [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
logarithm(x) → logIter(x, 0) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1]
if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
f → g [1]
f → h [1]

The TRS has the following type information:

half :: 0:s:logZeroError → 0:s:logZeroError 0 :: 0:s:logZeroError s :: 0:s:logZeroError → 0:s:logZeroError le :: 0:s:logZeroError → 0:s:logZeroError → true:false true :: true:false false :: true:false inc :: 0:s:logZeroError → 0:s:logZeroError logarithm :: 0:s:logZeroError → 0:s:logZeroError logIter :: 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError if :: true:false → true:false → 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError logZeroError :: 0:s:logZeroError f :: g:h g :: g:h h :: g:h

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

logarithm
logIter
if
f

(c) The following functions are completely defined:

le
half
inc

Due to the following rules being added:

le(v0, v1) → null_le [0]
half(v0) → null_half [0]
inc(v0) → null_inc [0]

And the following fresh constants:

null_le, null_half, null_inc

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: half(0) → 0 [1] half(s(0)) → 0 [1] half(s(s(x))) → s(half(x)) [1] le(0, y) → true [1] le(s(x), 0) → false [1] le(s(x), s(y)) → le(x, y) [1] inc(s(x)) → s(inc(x)) [1] inc(0) → s(0) [1] logarithm(x) → logIter(x, 0) [1] logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1] if(false, b, x, y) → logZeroError [1] if(true, false, x, s(y)) → y [1] if(true, true, x, y) → logIter(x, y) [1] f → g [1] f → h [1] le(v0, v1) → null_le [0] half(v0) → null_half [0] inc(v0) → null_inc [0] The TRS has the following type information: half :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc 0 :: 0:s:logZeroError:null_half:null_inc s :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc le :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc → true:false:null_le true :: true:false:null_le false :: true:false:null_le inc :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc logarithm :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc logIter :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc if :: true:false:null_le → true:false:null_le → 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc logZeroError :: 0:s:logZeroError:null_half:null_inc f :: g:h g :: g:h h :: g:h null_le :: true:false:null_le null_half :: 0:s:logZeroError:null_half:null_inc null_inc :: 0:s:logZeroError:null_half:null_inc Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: half(0) → 0 [1] half(s(0)) → 0 [1] half(s(s(x))) → s(half(x)) [1] le(0, y) → true [1] le(s(x), 0) → false [1] le(s(x), s(y)) → le(x, y) [1] inc(s(x)) → s(inc(x)) [1] inc(0) → s(0) [1] logarithm(x) → logIter(x, 0) [1] logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1] if(false, b, x, y) → logZeroError [1] if(true, false, x, s(y)) → y [1] if(true, true, x, y) → logIter(x, y) [1] f → g [1] f → h [1] le(v0, v1) → null_le [0] half(v0) → null_half [0] inc(v0) → null_inc [0] The TRS has the following type information: half :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc 0 :: 0:s:logZeroError:null_half:null_inc s :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc le :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc → true:false:null_le true :: true:false:null_le false :: true:false:null_le inc :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc logarithm :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc logIter :: 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc if :: true:false:null_le → true:false:null_le → 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc → 0:s:logZeroError:null_half:null_inc logZeroError :: 0:s:logZeroError:null_half:null_inc f :: g:h g :: g:h h :: g:h null_le :: true:false:null_le null_half :: 0:s:logZeroError:null_half:null_inc null_inc :: 0:s:logZeroError:null_half:null_inc Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
true => 2
false => 1
logZeroError => 1
g => 0
h => 1
null_le => 0
null_half => 0
null_inc => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
half(z) -{ 1 }→ 1 + half(x) :|: x >= 0, z = 1 + (1 + x)
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
inc(z) -{ 1 }→ 1 + inc(x) :|: x >= 0, z = 1 + x
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 2 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 1 :|: x >= 0, z = 1 + x, z' = 0
le(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
logIter(z, z') -{ 1 }→ if(le(1 + 0, x), le(1 + (1 + 0), x), half(x), inc(y)) :|: x >= 0, y >= 0, z = x, z' = y
logarithm(z) -{ 1 }→ logIter(x, 0) :|: x >= 0, z = x

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 1 }→ if(le(1 + 0, z), le(1 + (1 + 0), z), half(z), inc(z')) :|: z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ le } { f } { half } { inc } { logIter, if } { logarithm }

(14) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 1 }→ if(le(1 + 0, z), le(1 + (1 + 0), z), half(z), inc(z')) :|: z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {le}, {f}, {half}, {inc}, {logIter,if}, {logarithm}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: le
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 2

(16) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 1 }→ if(le(1 + 0, z), le(1 + (1 + 0), z), half(z), inc(z')) :|: z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {le}, {f}, {half}, {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: ?, size: O(1) [2]

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: le
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(18) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 1 }→ if(le(1 + 0, z), le(1 + (1 + 0), z), half(z), inc(z')) :|: z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {f}, {half}, {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2]

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·z }→ if(s', s'', half(z), inc(z')) :|: s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {f}, {half}, {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(22) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·z }→ if(s', s'', half(z), inc(z')) :|: s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {f}, {half}, {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: ?, size: O(1) [1]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: f
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(24) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·z }→ if(s', s'', half(z), inc(z')) :|: s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {half}, {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·z }→ if(s', s'', half(z), inc(z')) :|: s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {half}, {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(28) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·z }→ if(s', s'', half(z), inc(z')) :|: s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {half}, {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: ?, size: O(n1) [z]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(30) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·z }→ if(s', s'', half(z), inc(z')) :|: s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z]

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 4 + 3·z }→ if(s', s'', s2, inc(z')) :|: s2 >= 0, s2 <= 1 * z, s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: inc
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(34) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 4 + 3·z }→ if(s', s'', s2, inc(z')) :|: s2 >= 0, s2 <= 1 * z, s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {inc}, {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: ?, size: O(n1) [1 + z]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: inc
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(36) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 }→ 1 + inc(z - 1) :|: z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 4 + 3·z }→ if(s', s'', s2, inc(z')) :|: s2 >= 0, s2 <= 1 * z, s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 5 + 3·z + z' }→ if(s', s'', s2, s4) :|: s4 >= 0, s4 <= 1 * z' + 1, s2 >= 0, s2 <= 1 * z, s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: logIter
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

Computed SIZE bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(40) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 5 + 3·z + z' }→ if(s', s'', s2, s4) :|: s4 >= 0, s4 <= 1 * z' + 1, s2 >= 0, s2 <= 1 * z, s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z] logIter: runtime: ?, size: INF if: runtime: ?, size: INF

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: logIter
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(42) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ logIter(z'', z1) :|: z = 2, z' = 2, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ 1 :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
if(z, z', z'', z1) -{ 1 }→ z1 - 1 :|: z = 2, z'' >= 0, z1 - 1 >= 0, z' = 1
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 5 + 3·z + z' }→ if(s', s'', s2, s4) :|: s4 >= 0, s4 <= 1 * z' + 1, s2 >= 0, s2 <= 1 * z, s' >= 0, s' <= 2, s'' >= 0, s'' <= 2, z >= 0, z' >= 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z] logIter: runtime: INF, size: INF if: runtime: ?, size: INF

(43) RetryTechniqueProof (BOTH BOUNDS(ID, ID) transformation)

Performed narrowing of the following TRS rules:

if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1]

And obtained the following new TRS rules:

if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1]

Which were then size abstracted to RNTS rules to simplify the current SCC:

if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
logIter(z, z') -{ 1 }→ if(le(1 + 0, x), le(1 + (1 + 0), x), half(x), inc(y)) :|: x >= 0, y >= 0, z = x, z' = y

(44) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 1 }→ if(le(1 + 0, x), le(1 + (1 + 0), x), half(x), inc(y)) :|: x >= 0, y >= 0, z = x, z' = y
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z]

(45) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0

(46) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 4 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 5 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 3 + 3·x }→ if(s, s', 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 4 + 3·x + y }→ if(s, s', 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 3·x }→ if(s, s', 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(s, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(s, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 3 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 5 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 4 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(0, s, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(0, s, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(0, s, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 2 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 4 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0
logIter(z, z') -{ 1 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 1 + x }→ if(0, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 2 + x + y }→ if(0, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + x }→ if(0, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z]

(47) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(48) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 4 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 5 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 3 + 3·x }→ if(s, s', 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 4 + 3·x + y }→ if(s, s', 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 3·x }→ if(s, s', 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(s, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(s, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 3 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 5 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 4 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(0, s, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(0, s, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(0, s, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 2 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 4 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0
logIter(z, z') -{ 1 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 1 + x }→ if(0, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 2 + x + y }→ if(0, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + x }→ if(0, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z]

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: logIter
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

Computed SIZE bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'' + z1

(50) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 4 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 5 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 3 + 3·x }→ if(s, s', 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 4 + 3·x + y }→ if(s, s', 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 3·x }→ if(s, s', 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(s, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(s, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 3 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 5 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 4 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(0, s, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(0, s, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(0, s, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 2 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 4 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0
logIter(z, z') -{ 1 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 1 + x }→ if(0, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 2 + x + y }→ if(0, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + x }→ if(0, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logIter,if}, {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z] logIter: runtime: ?, size: O(n1) [1 + z + z'] if: runtime: ?, size: O(n1) [1 + z'' + z1]

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: logIter
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 10 + 14·z + 4·z·z' + 4·z² + 4·z'

Computed RUNTIME bound using PUBS for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 11 + 14·z'' + 4·z''·z1 + 4·z''² + 4·z1

(52) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 4 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 + 2·x + y }→ if(s, s', 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 5 + 2·x }→ if(s, s', 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 3 + 3·x }→ if(s, s', 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 4 + 3·x + y }→ if(s, s', 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + 3·x }→ if(s, s', 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(s, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(s, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(s, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(s, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(s, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 3 }→ if(1, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 5 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + y }→ if(1, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 5 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 4 }→ if(1, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(1, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 4 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(1, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(1, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 2 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 3 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 + x + y }→ if(0, s, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, y = 0
logIter(z, z') -{ 4 + x }→ if(0, s, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 2 + 2·x }→ if(0, s, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 3 + 2·x + y }→ if(0, s, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + 2·x }→ if(0, s, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 2 }→ if(0, 1, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 4 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 1, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 4 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 1, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0
logIter(z, z') -{ 1 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 + y }→ if(0, 0, 0, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, y = 0
logIter(z, z') -{ 2 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 3 }→ if(0, 0, 0, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 1 + x }→ if(0, 0, 1 + s1, 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 2 + x + y }→ if(0, 0, 1 + s1, 1 + s3) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 2 + x }→ if(0, 0, 1 + s1, 1 + 0) :|: x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logarithm(z) -{ 1 }→ logIter(z, 0) :|: z >= 0

Function symbols to be analyzed: {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z] logIter: runtime: O(n2) [10 + 14·z + 4·z·z' + 4·z2 + 4·z'], size: O(n1) [1 + z + z'] if: runtime: O(n2) [11 + 14·z'' + 4·z''·z1 + 4·z''2 + 4·z1], size: O(n1) [1 + z'' + z1]

(53) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(54) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 11 + 14·x + 4·x·y + 4·x² + 4·y }→ s2 :|: s2 >= 0, s2 <= 1 * y + 1 + 1 * x, z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 15 + 2·x }→ s10 :|: s10 >= 0, s10 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 20 + 4·s3 + 2·x + y }→ s11 :|: s11 >= 0, s11 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 20 + 2·x }→ s12 :|: s12 >= 0, s12 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 31 + 22·s1 + 4·s1² + 2·x }→ s13 :|: s13 >= 0, s13 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 2·x + y }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1² + 2·x }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 + x }→ s16 :|: s16 >= 0, s16 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 18 + 4·s3 + x + y }→ s17 :|: s17 >= 0, s17 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 + x }→ s18 :|: s18 >= 0, s18 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 14 + x }→ s19 :|: s19 >= 0, s19 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 19 + 4·s3 + x + y }→ s20 :|: s20 >= 0, s20 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + x }→ s21 :|: s21 >= 0, s21 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 15 }→ s22 :|: s22 >= 0, s22 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 20 + 4·s3 + y }→ s23 :|: s23 >= 0, s23 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 20 }→ s24 :|: s24 >= 0, s24 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 14 }→ s25 :|: s25 >= 0, s25 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s26 :|: s26 >= 0, s26 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s27 :|: s27 >= 0, s27 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 14 }→ s28 :|: s28 >= 0, s28 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s29 :|: s29 >= 0, s29 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s30 :|: s30 >= 0, s30 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 13 }→ s31 :|: s31 >= 0, s31 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s32 :|: s32 >= 0, s32 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s33 :|: s33 >= 0, s33 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 31 + 22·s1 + 4·s1² + 2·x }→ s34 :|: s34 >= 0, s34 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 2·x + y }→ s35 :|: s35 >= 0, s35 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1² + 2·x }→ s36 :|: s36 >= 0, s36 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 + x }→ s37 :|: s37 >= 0, s37 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0
logIter(z, z') -{ 18 + 4·s3 + x + y }→ s38 :|: s38 >= 0, s38 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 + x }→ s39 :|: s39 >= 0, s39 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, y = 0
logIter(z, z') -{ 32 + 22·s1 + 4·s1² + 3·x }→ s4 :|: s4 >= 0, s4 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 14 + x }→ s40 :|: s40 >= 0, s40 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 19 + 4·s3 + x + y }→ s41 :|: s41 >= 0, s41 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + x }→ s42 :|: s42 >= 0, s42 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 14 }→ s43 :|: s43 >= 0, s43 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s44 :|: s44 >= 0, s44 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s45 :|: s45 >= 0, s45 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 13 }→ s46 :|: s46 >= 0, s46 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s47 :|: s47 >= 0, s47 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s48 :|: s48 >= 0, s48 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 30 + 22·s1 + 4·s1² + x }→ s49 :|: s49 >= 0, s49 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 41 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 3·x + y }→ s5 :|: s5 >= 0, s5 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 39 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + x + y }→ s50 :|: s50 >= 0, s50 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 39 + 26·s1 + 4·s1² + x }→ s51 :|: s51 >= 0, s51 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 }→ s52 :|: s52 >= 0, s52 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s53 :|: s53 >= 0, s53 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s54 :|: s54 >= 0, s54 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, y = 0
logIter(z, z') -{ 12 }→ s55 :|: s55 >= 0, s55 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 17 + 4·s3 + y }→ s56 :|: s56 >= 0, s56 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 17 }→ s57 :|: s57 >= 0, s57 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 13 }→ s58 :|: s58 >= 0, s58 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s59 :|: s59 >= 0, s59 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 41 + 26·s1 + 4·s1² + 3·x }→ s6 :|: s6 >= 0, s6 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 18 }→ s60 :|: s60 >= 0, s60 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 14 + 2·x }→ s7 :|: s7 >= 0, s7 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 19 + 4·s3 + 2·x + y }→ s8 :|: s8 >= 0, s8 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + 2·x }→ s9 :|: s9 >= 0, s9 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, y = 0
logarithm(z) -{ 11 + 14·z + 4·z² }→ s'' :|: s'' >= 0, s'' <= 1 * 0 + 1 + 1 * z, z >= 0

Function symbols to be analyzed: {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z] logIter: runtime: O(n2) [10 + 14·z + 4·z·z' + 4·z2 + 4·z'], size: O(n1) [1 + z + z'] if: runtime: O(n2) [11 + 14·z'' + 4·z''·z1 + 4·z''2 + 4·z1], size: O(n1) [1 + z'' + z1]

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: logarithm
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(56) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 11 + 14·x + 4·x·y + 4·x² + 4·y }→ s2 :|: s2 >= 0, s2 <= 1 * y + 1 + 1 * x, z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 15 + 2·x }→ s10 :|: s10 >= 0, s10 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 20 + 4·s3 + 2·x + y }→ s11 :|: s11 >= 0, s11 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 20 + 2·x }→ s12 :|: s12 >= 0, s12 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 31 + 22·s1 + 4·s1² + 2·x }→ s13 :|: s13 >= 0, s13 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 2·x + y }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1² + 2·x }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 + x }→ s16 :|: s16 >= 0, s16 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 18 + 4·s3 + x + y }→ s17 :|: s17 >= 0, s17 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 + x }→ s18 :|: s18 >= 0, s18 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 14 + x }→ s19 :|: s19 >= 0, s19 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 19 + 4·s3 + x + y }→ s20 :|: s20 >= 0, s20 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + x }→ s21 :|: s21 >= 0, s21 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 15 }→ s22 :|: s22 >= 0, s22 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 20 + 4·s3 + y }→ s23 :|: s23 >= 0, s23 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 20 }→ s24 :|: s24 >= 0, s24 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 14 }→ s25 :|: s25 >= 0, s25 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s26 :|: s26 >= 0, s26 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s27 :|: s27 >= 0, s27 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 14 }→ s28 :|: s28 >= 0, s28 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s29 :|: s29 >= 0, s29 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s30 :|: s30 >= 0, s30 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 13 }→ s31 :|: s31 >= 0, s31 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s32 :|: s32 >= 0, s32 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s33 :|: s33 >= 0, s33 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 31 + 22·s1 + 4·s1² + 2·x }→ s34 :|: s34 >= 0, s34 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 2·x + y }→ s35 :|: s35 >= 0, s35 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1² + 2·x }→ s36 :|: s36 >= 0, s36 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 + x }→ s37 :|: s37 >= 0, s37 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0
logIter(z, z') -{ 18 + 4·s3 + x + y }→ s38 :|: s38 >= 0, s38 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 + x }→ s39 :|: s39 >= 0, s39 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, y = 0
logIter(z, z') -{ 32 + 22·s1 + 4·s1² + 3·x }→ s4 :|: s4 >= 0, s4 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 14 + x }→ s40 :|: s40 >= 0, s40 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 19 + 4·s3 + x + y }→ s41 :|: s41 >= 0, s41 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + x }→ s42 :|: s42 >= 0, s42 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 14 }→ s43 :|: s43 >= 0, s43 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s44 :|: s44 >= 0, s44 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s45 :|: s45 >= 0, s45 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 13 }→ s46 :|: s46 >= 0, s46 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s47 :|: s47 >= 0, s47 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s48 :|: s48 >= 0, s48 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 30 + 22·s1 + 4·s1² + x }→ s49 :|: s49 >= 0, s49 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 41 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 3·x + y }→ s5 :|: s5 >= 0, s5 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 39 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + x + y }→ s50 :|: s50 >= 0, s50 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 39 + 26·s1 + 4·s1² + x }→ s51 :|: s51 >= 0, s51 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 }→ s52 :|: s52 >= 0, s52 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s53 :|: s53 >= 0, s53 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s54 :|: s54 >= 0, s54 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, y = 0
logIter(z, z') -{ 12 }→ s55 :|: s55 >= 0, s55 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 17 + 4·s3 + y }→ s56 :|: s56 >= 0, s56 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 17 }→ s57 :|: s57 >= 0, s57 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 13 }→ s58 :|: s58 >= 0, s58 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s59 :|: s59 >= 0, s59 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 41 + 26·s1 + 4·s1² + 3·x }→ s6 :|: s6 >= 0, s6 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 18 }→ s60 :|: s60 >= 0, s60 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 14 + 2·x }→ s7 :|: s7 >= 0, s7 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 19 + 4·s3 + 2·x + y }→ s8 :|: s8 >= 0, s8 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + 2·x }→ s9 :|: s9 >= 0, s9 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, y = 0
logarithm(z) -{ 11 + 14·z + 4·z² }→ s'' :|: s'' >= 0, s'' <= 1 * 0 + 1 + 1 * z, z >= 0

Function symbols to be analyzed: {logarithm}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z] logIter: runtime: O(n2) [10 + 14·z + 4·z·z' + 4·z2 + 4·z'], size: O(n1) [1 + z + z'] if: runtime: O(n2) [11 + 14·z'' + 4·z''·z1 + 4·z''2 + 4·z1], size: O(n1) [1 + z'' + z1] logarithm: runtime: ?, size: O(n1) [1 + z]

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: logarithm
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 11 + 14·z + 4·z²

(58) Obligation:

Complexity RNTS consisting of the following rules:

f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 0 }→ 0 :|: z >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 2), z - 2 >= 0
if(z, z', z'', z1) -{ 11 + 14·x + 4·x·y + 4·x² + 4·y }→ s2 :|: s2 >= 0, s2 <= 1 * y + 1 + 1 * x, z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
inc(z) -{ 0 }→ 0 :|: z >= 0
inc(z) -{ 1 + z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 1) + 1, z - 1 >= 0
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 2, z - 1 >= 0, z' - 1 >= 0
le(z, z') -{ 1 }→ 2 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0
le(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
logIter(z, z') -{ 15 + 2·x }→ s10 :|: s10 >= 0, s10 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 20 + 4·s3 + 2·x + y }→ s11 :|: s11 >= 0, s11 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 20 + 2·x }→ s12 :|: s12 >= 0, s12 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 31 + 22·s1 + 4·s1² + 2·x }→ s13 :|: s13 >= 0, s13 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 2·x + y }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1² + 2·x }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 + x }→ s16 :|: s16 >= 0, s16 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 18 + 4·s3 + x + y }→ s17 :|: s17 >= 0, s17 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 + x }→ s18 :|: s18 >= 0, s18 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 14 + x }→ s19 :|: s19 >= 0, s19 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 19 + 4·s3 + x + y }→ s20 :|: s20 >= 0, s20 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + x }→ s21 :|: s21 >= 0, s21 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 15 }→ s22 :|: s22 >= 0, s22 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 20 + 4·s3 + y }→ s23 :|: s23 >= 0, s23 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 20 }→ s24 :|: s24 >= 0, s24 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 14 }→ s25 :|: s25 >= 0, s25 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s26 :|: s26 >= 0, s26 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s27 :|: s27 >= 0, s27 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) - 1 >= 0, y = 0
logIter(z, z') -{ 14 }→ s28 :|: s28 >= 0, s28 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s29 :|: s29 >= 0, s29 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s30 :|: s30 >= 0, s30 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 13 }→ s31 :|: s31 >= 0, s31 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s32 :|: s32 >= 0, s32 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s33 :|: s33 >= 0, s33 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 - 1 >= 0, x = 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 31 + 22·s1 + 4·s1² + 2·x }→ s34 :|: s34 >= 0, s34 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 2·x + y }→ s35 :|: s35 >= 0, s35 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 40 + 26·s1 + 4·s1² + 2·x }→ s36 :|: s36 >= 0, s36 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 + x }→ s37 :|: s37 >= 0, s37 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0
logIter(z, z') -{ 18 + 4·s3 + x + y }→ s38 :|: s38 >= 0, s38 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 + x }→ s39 :|: s39 >= 0, s39 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, y = 0
logIter(z, z') -{ 32 + 22·s1 + 4·s1² + 3·x }→ s4 :|: s4 >= 0, s4 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 14 + x }→ s40 :|: s40 >= 0, s40 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0
logIter(z, z') -{ 19 + 4·s3 + x + y }→ s41 :|: s41 >= 0, s41 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + x }→ s42 :|: s42 >= 0, s42 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, s >= 0, s <= 2, 1 + (1 + 0) - 1 >= 0, x - 1 >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 14 }→ s43 :|: s43 >= 0, s43 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 19 + 4·s3 + y }→ s44 :|: s44 >= 0, s44 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 }→ s45 :|: s45 >= 0, s45 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 13 }→ s46 :|: s46 >= 0, s46 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s47 :|: s47 >= 0, s47 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s48 :|: s48 >= 0, s48 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) - 1 >= 0, x = 0, y = 0
logIter(z, z') -{ 30 + 22·s1 + 4·s1² + x }→ s49 :|: s49 >= 0, s49 <= 1 * (1 + s1) + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0
logIter(z, z') -{ 41 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + 3·x + y }→ s5 :|: s5 >= 0, s5 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 39 + 26·s1 + 4·s1·s3 + 4·s1² + 8·s3 + x + y }→ s50 :|: s50 >= 0, s50 <= 1 * (1 + s1) + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 39 + 26·s1 + 4·s1² + x }→ s51 :|: s51 >= 0, s51 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 13 }→ s52 :|: s52 >= 0, s52 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s53 :|: s53 >= 0, s53 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 18 }→ s54 :|: s54 >= 0, s54 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 0, y = 0
logIter(z, z') -{ 12 }→ s55 :|: s55 >= 0, s55 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0
logIter(z, z') -{ 17 + 4·s3 + y }→ s56 :|: s56 >= 0, s56 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 17 }→ s57 :|: s57 >= 0, s57 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, y = 0
logIter(z, z') -{ 13 }→ s58 :|: s58 >= 0, s58 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0
logIter(z, z') -{ 18 + 4·s3 + y }→ s59 :|: s59 >= 0, s59 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 41 + 26·s1 + 4·s1² + 3·x }→ s6 :|: s6 >= 0, s6 <= 1 * (1 + s1) + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s1 >= 0, s1 <= 1 * (x - 2), x - 2 >= 0, y = 0
logIter(z, z') -{ 18 }→ s60 :|: s60 >= 0, s60 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, 1 + 0 >= 0, 1 + (1 + 0) >= 0, x = 1 + 0, y = 0
logIter(z, z') -{ 14 + 2·x }→ s7 :|: s7 >= 0, s7 <= 1 * 0 + 1 * 0 + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0
logIter(z, z') -{ 19 + 4·s3 + 2·x + y }→ s8 :|: s8 >= 0, s8 <= 1 * 0 + 1 * (1 + s3) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, s3 >= 0, s3 <= 1 * (y - 1) + 1, y - 1 >= 0
logIter(z, z') -{ 19 + 2·x }→ s9 :|: s9 >= 0, s9 <= 1 * 0 + 1 * (1 + 0) + 1, x >= 0, y >= 0, z = x, z' = y, s >= 0, s <= 2, 1 + 0 - 1 >= 0, x - 1 >= 0, s' >= 0, s' <= 2, 1 + (1 + 0) - 1 >= 0, y = 0
logarithm(z) -{ 11 + 14·z + 4·z² }→ s'' :|: s'' >= 0, s'' <= 1 * 0 + 1 + 1 * z, z >= 0

Function symbols to be analyzed:
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [2] f: runtime: O(1) [1], size: O(1) [1] half: runtime: O(n1) [1 + z], size: O(n1) [z] inc: runtime: O(n1) [1 + z], size: O(n1) [1 + z] logIter: runtime: O(n2) [10 + 14·z + 4·z·z' + 4·z2 + 4·z'], size: O(n1) [1 + z + z'] if: runtime: O(n2) [11 + 14·z'' + 4·z''·z1 + 4·z''2 + 4·z1], size: O(n1) [1 + z'' + z1] logarithm: runtime: O(n2) [11 + 14·z + 4·z2], size: O(n1) [1 + z]

(59) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(60) BOUNDS(1, n^2)